init\_p(${\it es}$; $i$; $T$; $x$; $v$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); $T$) c$\wedge$ (es\_init(${\it es}$)($i$,$x$) = $v$ $\in$ rationals$\rightarrow$$T$)